0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 83 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 0 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 0 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 PiDP
↳9 UsableRulesProof (⇔, 0 ms)
↳10 PiDP
↳11 PiDPToQDPProof (⇒, 12 ms)
↳12 QDP
↳13 QDPSizeChangeProof (⇔, 0 ms)
↳14 YES
memberA_in_ag(T5, .(T5, T6)) → memberA_out_ag(T5, .(T5, T6))
memberA_in_ag(T22, .(T11, .(T22, T23))) → memberA_out_ag(T22, .(T11, .(T22, T23)))
memberA_in_ag(T33, .(T11, .(T31, T32))) → U1_ag(T33, T11, T31, T32, memberA_in_ag(T33, T32))
memberA_in_ag(T64, .(T42, .(T62, T63))) → U2_ag(T64, T42, T62, T63, memberA_in_ag(T64, T63))
U2_ag(T64, T42, T62, T63, memberA_out_ag(T64, T63)) → memberA_out_ag(T64, .(T42, .(T62, T63)))
U1_ag(T33, T11, T31, T32, memberA_out_ag(T33, T32)) → memberA_out_ag(T33, .(T11, .(T31, T32)))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
memberA_in_ag(T5, .(T5, T6)) → memberA_out_ag(T5, .(T5, T6))
memberA_in_ag(T22, .(T11, .(T22, T23))) → memberA_out_ag(T22, .(T11, .(T22, T23)))
memberA_in_ag(T33, .(T11, .(T31, T32))) → U1_ag(T33, T11, T31, T32, memberA_in_ag(T33, T32))
memberA_in_ag(T64, .(T42, .(T62, T63))) → U2_ag(T64, T42, T62, T63, memberA_in_ag(T64, T63))
U2_ag(T64, T42, T62, T63, memberA_out_ag(T64, T63)) → memberA_out_ag(T64, .(T42, .(T62, T63)))
U1_ag(T33, T11, T31, T32, memberA_out_ag(T33, T32)) → memberA_out_ag(T33, .(T11, .(T31, T32)))
MEMBERA_IN_AG(T33, .(T11, .(T31, T32))) → U1_AG(T33, T11, T31, T32, memberA_in_ag(T33, T32))
MEMBERA_IN_AG(T33, .(T11, .(T31, T32))) → MEMBERA_IN_AG(T33, T32)
MEMBERA_IN_AG(T64, .(T42, .(T62, T63))) → U2_AG(T64, T42, T62, T63, memberA_in_ag(T64, T63))
memberA_in_ag(T5, .(T5, T6)) → memberA_out_ag(T5, .(T5, T6))
memberA_in_ag(T22, .(T11, .(T22, T23))) → memberA_out_ag(T22, .(T11, .(T22, T23)))
memberA_in_ag(T33, .(T11, .(T31, T32))) → U1_ag(T33, T11, T31, T32, memberA_in_ag(T33, T32))
memberA_in_ag(T64, .(T42, .(T62, T63))) → U2_ag(T64, T42, T62, T63, memberA_in_ag(T64, T63))
U2_ag(T64, T42, T62, T63, memberA_out_ag(T64, T63)) → memberA_out_ag(T64, .(T42, .(T62, T63)))
U1_ag(T33, T11, T31, T32, memberA_out_ag(T33, T32)) → memberA_out_ag(T33, .(T11, .(T31, T32)))
MEMBERA_IN_AG(T33, .(T11, .(T31, T32))) → U1_AG(T33, T11, T31, T32, memberA_in_ag(T33, T32))
MEMBERA_IN_AG(T33, .(T11, .(T31, T32))) → MEMBERA_IN_AG(T33, T32)
MEMBERA_IN_AG(T64, .(T42, .(T62, T63))) → U2_AG(T64, T42, T62, T63, memberA_in_ag(T64, T63))
memberA_in_ag(T5, .(T5, T6)) → memberA_out_ag(T5, .(T5, T6))
memberA_in_ag(T22, .(T11, .(T22, T23))) → memberA_out_ag(T22, .(T11, .(T22, T23)))
memberA_in_ag(T33, .(T11, .(T31, T32))) → U1_ag(T33, T11, T31, T32, memberA_in_ag(T33, T32))
memberA_in_ag(T64, .(T42, .(T62, T63))) → U2_ag(T64, T42, T62, T63, memberA_in_ag(T64, T63))
U2_ag(T64, T42, T62, T63, memberA_out_ag(T64, T63)) → memberA_out_ag(T64, .(T42, .(T62, T63)))
U1_ag(T33, T11, T31, T32, memberA_out_ag(T33, T32)) → memberA_out_ag(T33, .(T11, .(T31, T32)))
MEMBERA_IN_AG(T33, .(T11, .(T31, T32))) → MEMBERA_IN_AG(T33, T32)
memberA_in_ag(T5, .(T5, T6)) → memberA_out_ag(T5, .(T5, T6))
memberA_in_ag(T22, .(T11, .(T22, T23))) → memberA_out_ag(T22, .(T11, .(T22, T23)))
memberA_in_ag(T33, .(T11, .(T31, T32))) → U1_ag(T33, T11, T31, T32, memberA_in_ag(T33, T32))
memberA_in_ag(T64, .(T42, .(T62, T63))) → U2_ag(T64, T42, T62, T63, memberA_in_ag(T64, T63))
U2_ag(T64, T42, T62, T63, memberA_out_ag(T64, T63)) → memberA_out_ag(T64, .(T42, .(T62, T63)))
U1_ag(T33, T11, T31, T32, memberA_out_ag(T33, T32)) → memberA_out_ag(T33, .(T11, .(T31, T32)))
MEMBERA_IN_AG(T33, .(T11, .(T31, T32))) → MEMBERA_IN_AG(T33, T32)
MEMBERA_IN_AG(.(T11, .(T31, T32))) → MEMBERA_IN_AG(T32)
From the DPs we obtained the following set of size-change graphs: